COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	\magnify{1100}
C00010 ENDMK
C⊗;
\magnify{1100}
\catcode`|=13
\def|#1|{\hbox{\it#1\/}}
\parindent 0pt
\parskip 0pt
\def\pskip{\penalty-1000\vskip 6pt plus 2pt minus 1pt}
\def\ppskip{\penalty-2000\vskip 10pt plus 3pt minus 2pt}
\def\no(#1){\noindent\hbox to 6em{(#1)\hfill}}
\catcode`⊗=13
\def⊗{\hbox to 2em{}}
\def\IF{\mathop{\bf if}}
\def\THEN{\mathrel{\bf then}}
\def\ELSE{\mathrel{\bf else}}
\def\AND{\mathrel{\bf and}}
\def\OR{\mathrel{\bf or}}
\def\NOT{\mathop{\bf not}}
\def\N{\mathop{\bf n}}
\def\T{\hbox{\tt T}}
\def\NIL{\hbox{\tt NIL}}
\def\.{\mathbin{.}}
\def\A{\mathop{\bf a}}
\def\D{\mathop{\bf d}}
\def\EQ{\mathrel{\bf eq}}
\def\AT{\mathop{\bf at}}
\def\quote#1{\hbox{\sfcode`.=1000\tt#1}}
\def\list#1{\langle#1\rangle}

\ctrline{CS 206---Recursive Programming and Proving}
\ctrline{Midterm Exam Solutions}
\ctrline{Tuesday, November 23, 1982}

\ppskip
\no(1)$|isordered|\,u←$\par
$⊗⊗⊗⊗\IF\N u\OR\N\D u\THEN\T$\par
$⊗⊗⊗⊗\ELSE\IF\A u>\A\D u\THEN\NIL$\par
$⊗⊗⊗⊗\ELSE |isordered|\,\D u$\par
\pskip
$⊗⊗⊗|isordered|\,u←\N u\OR\N\D u\OR(\A u≤\A\D u\AND |isordered|\,\D u)$\par
\pskip
The problem didn't mention whether a list like \quote{(2 3 3)} should be
considered ordered or not, so no points were taken off for using $<$ instead
of $≤$ or vice versa.  The most common error was not terminating when
$\N\D u$ is true, since then the function will try to take $\A\D u$, which
is undefined.  It is also a good idea to test for $\N u$, in case the
original input list is \NIL; this should be considered to be an ordered list.

\ppskip
\no(2)$|remove|[x,u]←$\par
$⊗⊗⊗⊗\IF\N u\THEN\NIL$\par
$⊗⊗⊗⊗\ELSE\IF x=\A u\THEN |remove|[x,\D u]$\par
$⊗⊗⊗⊗\ELSE\A u\.|remove|[x,\D u]$\par
\pskip
Recall that
\pskip
$⊗⊗⊗|member|[x,u]←\NOT\N u\AND[[x=\A u]\OR|member|[x,\D u]].$\par
\pskip
The proof in part (b) is by list induction on the formula $\Phi(u)$:
$|member|[x,|remove|[x,u]]=\NIL$.  The proof will not make any assumptions
about $x$, so a $∀x$ quantifier may be added at the end.  Either form of
the list induction principle may be used.  First let us use
$$\Phi(\NIL)∧(∀u.\,¬\N u∧\Phi(\D u)⊃\Phi(u))⊃∀u.\,\Phi(u).$$
We can see that
$\Phi(\NIL)$ is true because $|remove|[x,\NIL]=\NIL$ by the definition of
|remove|; thus
\pskip
$⊗⊗⊗|member|[x,|remove|[x,\NIL]]=|member|[x,\NIL]$\par
$⊗⊗⊗⊗=\NIL,$\par
\pskip
by expanding the definition of |member|.  Now, 
using the assumptions $¬\N u$ and $\Phi(\D u)$, which is
$|member|[x,|remove|[x,\D u]]=\NIL$, we compute $|member|[x,|remove|[x,u]]$
by first expanding the |remove| and simplifying:
\pskip
$⊗⊗⊗|member|[x,|remove|[x,u]]$\par
$⊗⊗⊗⊗=\IF x=\A u\THEN|member|[x,|remove|[x,\D u]]$\par
$⊗⊗⊗⊗⊗\ELSE|member|[x,\A u\.|remove|[x,\D u]]$\par
\pskip
Now we use the inductive hypothesis to replace $|member|[x,|remove|[x,\D u]]$
by \NIL, and expand the oter use of |member|:
\pskip
$⊗⊗⊗⊗=\IF x=\A u\THEN\NIL\ELSE [x=\A u]\OR|member|[x,|remove|[x,\D u]]$\par
$⊗⊗⊗⊗=\NIL.$\par
\pskip
The second occurrence of $x=\A u$ in the line above can be replaced by \NIL,
since it occurs in a context where $x=\A u$ is known to be false.
\pskip
The other form of the list induction principle is
$$\Phi(\NIL)∧(∀y\,u.\,\Phi(u)⊃\Phi(y\.u))⊃∀u.\,\Phi(u).$$
The variable $y$ is used instead of the usual $x$ because $x$ is already in
use as the first argument to |remove| and |member|.  The proof of
$\Phi(\NIL)$ is the
same as before, and using the assumption $\Phi(u)$, we have
\pskip
$⊗⊗⊗|member|[x,|remove|[x,y\.u]$\par
$⊗⊗⊗⊗=\IF x=y\THEN|member|[x,|remove|[x,u]]$\par
$⊗⊗⊗⊗⊗\ELSE|member|[x,y\.|remove|[x,u]]$\par
$⊗⊗⊗⊗=\IF x=y\THEN\NIL\ELSE [x=y]\OR|member|[x,|remove|[x,u]]$\par
$⊗⊗⊗⊗=\NIL,$
\pskip
using the same steps as in the previous version of the proof.

\ppskip
\no(3)$g[n]←\IF n≥0\AND |odd|[n]\THEN 0\ELSE\bot,$\par
$⊗⊗⊗h[n]←\IF n≥0\THEN 0\ELSE\bot.$\par
\pskip
Of the six statements in part (b), only (iii) and (v) are true.  The
functions $f$ and $g$ each are defined for values at which the other is
not defined, hence $f\sqsub g$ and $g\sqsub f$ are both false.

\ppskip
\no(4)$|simplify|\,|spexp|←$\par
$⊗⊗⊗⊗\IF\AT|spexp|\THEN|spexp|$\par
$⊗⊗⊗⊗\ELSE\IF\A|spexp|=\quote{PLUS}\THEN$\par
$⊗⊗⊗⊗⊗[λu.\,\IF\N u\THEN 0\ELSE\IF\N\D u\THEN\A u\ELSE\quote{PLUS}\.u]
	[|simplus|\,\D|spexp|]$\par
$⊗⊗⊗⊗\ELSE\IF\A|spexp|=\quote{TIMES}\THEN$\par
$⊗⊗⊗⊗⊗[λu.\,\IF u=0\THEN 0$\par
$⊗⊗⊗⊗⊗⊗\ELSE\IF\N u\THEN 1$\par
$⊗⊗⊗⊗⊗⊗\ELSE\IF\N\D u\THEN\A u$\par
$⊗⊗⊗⊗⊗⊗\ELSE\quote{TIMES}\.u][|simtimes|\,\D|spexp|]$\par
\pskip
$⊗⊗⊗|simplus|\,u←$\par
$⊗⊗⊗⊗\IF\N u\THEN\NIL$\par
$⊗⊗⊗⊗\ELSE[λe.\,\IF e=0\THEN|simplus|\,\D u\ELSE e\.|simplus|\,\D u]
	\,[|simplify|\,\A u]$\par
\pskip
$⊗⊗⊗|simtimes|\,u←$\par
$⊗⊗⊗⊗\IF\N u\THEN\NIL$\par
$⊗⊗⊗⊗\ELSE[λe.\,\IF e=0\THEN 0$\par
$⊗⊗⊗⊗⊗⊗\ELSE\IF e=1\THEN|simtimes|\,\D u$\par
$⊗⊗⊗⊗⊗⊗\ELSE[λv.\,\IF v=0\THEN 0\ELSE e\.v][|simtimes|\,\D u]]
	\,[|simplify|\,\A u]$\par

\vfill\end